M:(IdLnkIdType), rt:(IdId), rtinv:(Id(Id+Unit)).
inv-rel(Id;Id;rt;rtinv)
 (m:Msg(M). isl(rtinv(mtag(m)))  msg-rename(rtinv;m)  Msg(l,tg. M(l,rt(tg)))) 

latex

Definitions	P & Q, True, False, outl(x), P  Q, msg-rename(rtinv;m), b, isl(x), mtag(m), Msg(M), inv-rel(A;B;f;finv), x:A. B(x), Unit, IdLnk, Id, t  T
Lemmas	Id wf, IdLnk wf, unit wf, inv-rel wf, Msg wf, mtag wf, isl wf, assert wf, outl wf, false wf, true wf